All Thinking Things
"What we want is a machine that can learn from experience. The possibility of letting the machine alter its own instructions provides the mechanism for this."
— Alan Turing, London Mathematical Society, February 1947
In 1952 Alan Turing played a game of chess against his colleague Alick Glennie. He did so by taking on the role of a computer: he had written a chess program on a few sheets of paper, and at every turn he followed the instructions of his program to the letter, until they produced a move. Every move took him about half an hour. He lost.
Throughout that game, Alan did exactly what a computer does. He carried out the program faithfully, without improving a line of it, however obvious the improvements must sometimes have looked.
Promptly thereafter, the machines arrived. And programming settled into a division of labour that has held ever since: Human beings decide, and write down, precisely what a program should do. A computer then carries it out, instruction by instruction and billions of times a second, exactly as written. Any and all thinking happens before the program is executed, but absolutely none during or after.
In the last few years AI has joined the fray. AI models now draft code with programmers, and since the November singularity, increasingly for them. But the code they write still goes to the same computers, which carry it out mechanically, deterministically, and unthinkingly, in much the same way Turing did with his chess program.
Why has AI thus far been relegated only to help write code, but never to help execute it?
Had Turing been free to act on what he saw at the board, he could have improved his program with every move, and it would have played a little better each time. Analogously, every piece of computer code, coupled with full “contextual knowledge” of the environment and conditions under which it is executed, and the flow of data through it, could be accelerated, made to use fewer resources, or otherwise improved.
At doubleAI we have built a new category of models to do exactly this.
We call them code execution models, or CEMs. They place artificial intelligence somewhere it has never been before: between code and silicon. CEMs work under wholly different constraints from models that write code. A CEM lives inside the running program, watching the data flow through it and reshaping the algorithms and instructions as it goes. The output is a binary, run directly on the hardware. No humans in the loop. Therefore, the model must never err. To date, no AI has made that promise. Read on to see how we do so.
Proofs, Mathematics, and Code
Very recently formal verification¹ has revolutionised mathematics. Anthropic published a complete, 13-million-line formal proof of Fermat's Last Theorem.² Four days after Anthropic's proof appeared, OpenAI published a finite-time blow-up result for the Navier–Stokes equations, one of the Millennium Prize problems, again backed by a complete formal proof. Since then, AI-written formal proofs of important results have been appearing at a dizzying rate. Mathematics itself is seemingly being remade.
This raises the question: can the same be done for software? For a CEM, this question is crucial. After all, a CEM evolves running programs, often many times a day, without any human reviewer in the loop. Even if there were time for it, rote testing would not be sufficient. What does it take to do this safely?
The answer is the same tool that is now remaking mathematics: formal verification. The first step is to formalise the code, giving it a precise mathematical meaning that a machine can reason about. From then on, any question about how the code behaves can be settled by proof.
Our first CEM, which we are releasing for early access, is called Maxwell’s Daemon³, or more casually, Maxwell. Its goal is superoptimisation: finding the fastest possible way to carry out a piece of code on the machine in front of it. Maxwell takes existing code and, while the program is running, modifies the algorithms and the machine instructions, emitting new binary code, much as a just-in-time compiler does, though with far more freedom in what the new algorithm may look like.⁴ Any replacement it makes must be precisely semantically equivalent to the code that preceded it.
Crucially, nothing changes in the source code. Rather, what changes is what runs underneath: much faster binaries, proven to be exactly equivalent to those that they replace. While a program runs, Maxwell identifies its bottlenecks, along with the ways in which they are expressed. For each bottleneck it finds, Maxwell creates a new version, assembled for the exact machine on which it is running. The source code stays exactly as its authors wrote it, whether they are human or a coding agent such as Claude Code. Maxwell is therefore complementary to coding agents: they write the program, and Maxwell makes sure the machine runs it optimally.
For Maxwell, formal verification takes the form of formal proofs of semantic equivalence.
Two programs are semantically equivalent when, given the same input, they always produce the same result and have the same effect on the world around them. They may look nothing alike. One might be a few lines of Python and the other some Rust or C code. What matters is that nobody using them, no matter how hard they try, is able to tell them apart (except, of course, that one is much more efficient). A formal proof of equivalence establishes this for every possible input and every possible scenario at once, in a language precise enough for a machine to check every step.⁵
Original
def original(n): s = 0 for i in range(n): for j in range(i): s += 1 return s
Replacement
fn replacement(n: i64) -> i64 {
n * (n - 1) / 2
}Proof of equivalence
requires n : int 0 ≤ n ≤ 3037000500 theorem original(n) = replacement(n) by induction on n case 0: original(0) = 0 = replacement(0) case n + 1: original(n + 1) = original(n) + n = n(n − 1)/2 + n = (n + 1)n/2 = replacement(n + 1) ∎
There is a deep and well-known connection between programs and proofs, known as the Curry–Howard correspondence. Essentially, a proof is a program, and checking a proof amounts to checking that the program is correctly put together. More concretely, most programming languages are underpinned by types, which describe what “kind of thing” a value is (for example, a number or a piece of text). The correspondence observes that a type can just as well describe a mathematical statement, and that a program producing a value of that type is then a proof of the statement. Much in the same way, through this correspondence, a lemma becomes a small function, and a theorem built from lemmas becomes a larger program that calls them. Checking the proof is then nothing more than type-checking the program. This is type theory (in a nutshell), the mechanism on top of which most modern proof checkers are built.
At doubleAI we have made a number of breakthroughs in formally verified code.
One such breakthrough is our complete formalisation of the Python programming language, among the most dynamic languages there are.
Why is Python so difficult to formalise? In Python a value can change type from one line to the next. In fact, Python is so dynamic that even basic principles, such as what a number is, and what it means to add two of them up, can be wholly redefined while the program is running. This dynamic nature is part of what makes Python such an appealing programming ecosystem.
Our formalisation accounts for all of this behaviour. It covers not just small, self-contained functions that formal methods have traditionally been limited to. Rather, it covers ordinary, general-purpose Python as it exists in the real world, including code that performs communication, uses files, and so forth. With Python formalised, the claim that a piece of Python and a rewritten version of it agree can itself be written down formally, and proved.
Part of what makes Maxwell so potent is that it is trained at doubleAI to work within this formal system, writing each piece of new code alongside its formal proof of semantic equivalence.
Writing such proofs may sound like an enormous undertaking. For a person, it would be. Maxwell is not a person. Its proofs are largely built from reusable proof gadgets, each proved only once. Proofs also compose, so a proof for an entire unit can be assembled from many small ones. What is left is meticulous, tedious work; exactly the kind at which AI far surpasses human beings.
Maxwell handles both CPU and GPU code. Python code gets swapped for low-level, bare-metal optimised code (including, for instance, direct SIMD implementations, wherever relevant). PyTorch code similarly gets replaced with highly optimised kernels for the particular GPU present on the machine. The optimisations are far-reaching and encompass many more moving parts across the Python ecosystem.
One of the key enablers for optimisation is the contextual information about how programs are run. This lets Maxwell specialise code to what it has actually observed, while of course guarding against the scenario in which any of the assumed preconditions has changed. Because every acceleration comes with a machine-checked proof, Maxwell can afford to be brave, taking on transformations that no compiler or human engineer would risk, while being absolutely sure of their correctness, always.
Building a CEM like Maxwell comes with a great deal of engineering. Maxwell has to slip seamlessly into the runtime, detect bottlenecks, and accelerate code throughout, all without ever slowing down the “hot path”. Each of these is a story of its own, but perhaps one best left for another day.
Maxwell: An Agent for the Machine
Until now, AI in software has worked for programmers, writing code at their request and then stepping away. Maxwell lives with the code. It works for as long as the program runs, on behalf of the machine it runs on. It sees the hardware the program has landed on and the exact shapes and types of the data flowing through it, and it keeps fitting the code to both as they change.
Once Maxwell has proved a faster version of some code, that version becomes the starting point for its next attempt, and the program keeps getting faster for as long as it runs, while its source stays exactly as its authors left it. We think of this as self-improving code. Maxwell can bring this to every machine it runs on, at internet scale.
We think this matters well beyond any single program. Computing power has become one of the scarcest resources in the world, and much of it goes to running code far more slowly than it could run. Every program Maxwell speeds up gives some of that back. Maxwell will be available soon, in early access. We are very excited to see what a world full of Maxwells looks like.
In 1952, Turing had to follow his program exactly as written. Our machines no longer have to.
¹ Formal verification is the practice of writing a proof in a language precise enough for a computer to check every step.
² The proof was written by Anthropic's AI agents over the span of eleven days. Formalising the theorem had previously been the goal of a five-year, publicly funded programme that a group of top human mathematicians began in 2024.
³ After the tiny creature James Clerk Maxwell imagined in 1867, which lowered the entropy of a gas simply by sorting its molecules. Our Maxwell brings the same kind of order to code, fitting it to your hardware, your data and the way you use it.
⁴ Compilers and just-in-time compilers, such as torch.compile and PyPy, are limited to transformations written in advance by their engineers, and superoptimisers such as STOKE to short, loop-free fragments of machine code, optimised once, statically. Maxwell rewrites entire functions, algorithms included, inside real-world programs as they run. It fits each version to the exact hardware and to the data actually flowing through the program, keeps re-optimising as either changes, and proves every piece of code equivalent, rather than testing it.
⁵ Rice's theorem tells us that no algorithm can decide semantic equivalence for every pair of programs. That is a limit on a universal procedure, however, and says nothing about the particular pair in front of you. In practice, for nearly any two equivalent programs that we care about, such a claim can be written down formally, as a proof.
